In electronic design automation processes, logic synthesis generally refers to the conversion of a high-level specification of a circuit design into a gate-level netlist, which typically describes the components to be used to implement the design and the connections between these components. One example of a high-level specification of the circuit design is a description of the functionality of the design in the register transfer level (RTL), such as description of how data is moved between registers and memory, how data is manipulated (e.g., by adding, by comparing, etc.), where data is stored (e.g., in some registers or memory locations), etc. In general, the RTL description may be written in a hardware description language (HDL). The HDL may handle several levels of abstraction, such as behavioral level, register transfer level, and gate levels. One example of the HDL is Verilog.
The netlist generated by logic synthesis may be written in various formats, such as in graphical format or in textual format, to represent the circuit that implements the high-level specification. Some conventional synthesis tools further optimize different portions of a design for a variety of attributes, such as area, speed, etc. For example, one conventional logic synthesis tool may optimize a portion of a design for area by using the smallest amount of area on a silicon chip while another conventional synthesis tool may optimize a portion of a design for speed by adding or removing some logic gates in the netlist. As a result, multiple netlists to achieve the same functionality described by the high-level specification may be generated for different kinds of optimization.
Furthermore, as new technologies in electronic device processing areb being developed to build smaller, faster, and better integrated circuits, netlists of alternative implementations may be generated by logic synthesis based on different fabrication processing technologies. These alternative implementations of the design may take advantage of some or all of these new technologies. The netlists may use different combinations of logic gates, electronic components, wire, etc. to achieve the same functionality as described in the high-level specification.
To ensure the accuracy of the logic synthesis performed, there is a need to verify that the different netlists indeed achieve the same functionality as specified. In other words, it is desired to have an efficient and accurate methodology to verify that a logic synthesis tool indeed preserves the high-level specification in an alternative implementation of the design.
Currently, a sequential circuit is a network of combinational sub-circuits implementing some next-state functions. If a combinational sub-circuit is large enough, it usually can be further partitioned into smaller sub-circuits. It was shown in Equivalence checking of dissimilar circuits. E. Goldberg, Y. Novikov, International Workshop on Logic and Synthesis, May 28-30, 2003, USA that the knowledge of a high-level level structure of a circuit is crucial for efficient Equivalence Checking (EC). Namely, it was shown that if two combinational circuits N1,N2 have a Common Specification (CS), then there exists an efficient procedure for checking their equivalence.
A common specification S of N1 and N2 is typically defined as a circuit of multi-valued gates (which may also be referred to as blocks) such that N1 and N2 are different implementations of S. An example of a CS is given in FIG. 1. Circuits N1 1001 and N2 1002 have a 3-block CS 1000 shown on the left. Sub-circuits N1i, N2i (where i=1, 2, or 3) are different implementations of the multi-valued block, Gi of S. Circuit Nmi (m=1, 2) implements a multi-output Boolean function whose truth table is obtained from that of Gi by replacing values of multi-valued variables with their binary codes. So the difference between N1i and N2i is in the choice of binary encodings for the variables of S.
In general, equivalence checking of circuits N1, N2 with a common specification S is typically infeasible if the common specification S is unknown. However, if the common specification S is known, then there may exist an efficient procedure for performing the equivalence checking of circuits N1, N2. This equivalence checking procedure can be used to design a new class of logic synthesis procedures. In general, a logic synthesis procedure has to verify that the original circuit N1 and a changed circuit N2 are functionally equivalent, i.e., to verify the change made from circuits N1 to N2. The more powerful this verification procedure is, the richer set of synthesis transformations can be used. So any progress in equivalence checking entails introducing a new class of synthesis transformations.